"""
样例输入
p, ~q, ~p|~r|q
r
p|q, ~p|r, ~q|r
~r
p, ~p|q, ~p|~q|r
p, r

样例输出
TRUE
TRUE
FALSE
"""

# from collections import defaultdict

S = []
T = dict()
F = dict()
U = dict()


def read_clause(line, reverse=False):
    line = line.replace(' ', '').strip()
    line = line.split('|')
    if reverse:
        line = [opposite(_) for _ in line]
    S.append(line)


def opposite(clause):
    if '~' in clause:
        return clause.replace('~', '')
    else:
        return '~' + clause


def resolution():
    global S
    end = False

    ret = []
    while S:
        if end: break
        father = S.pop()
        for i in father[:]:
            if end: break
            for mother in S[:]:
                if end:
                    break
                j = list(filter(lambda x: x == opposite(i), mother))
                if j == []:
                    continue
                else:
                    # print('\n亲本子句：' + ' ∨ '.join(father) + ' 和 ' + ' ∨ '.join(mother))
                    father.remove(i)
                    mother.remove(j[0])
                    if father == [] and mother == []:
                        # print('归结式：NIL')
                        end = True
                    elif father == []:
                        # print('归结式：' + '|'.join(mother))
                        ret.append('|'.join(mother))
                    elif mother == []:
                        # print('归结式：' + '|'.join(father))
                        ret.append('|'.join(father))
                    else:
                        # print('归结式：' + '|'.join(father) + '|' + '|'.join(mother))
                        ret.append('|'.join(father) + '|' + '|'.join(mother))
    return ret


s1 = "p, ~q, ~p|~r|q"
s2 = "r"

s1 = "p|q, ~p|r, ~q|r"
s2 = "~r"

s1 = "p, ~p|q, ~p|~q|r"
s2 = "p, r"


for one in s1.split(","):
    read_clause(one)
# for one in s2.split(","):
#     read_clause(one, True)
# print(S)
results = resolution()

f = True
for one in s2.split(","):
    one.replace(' ', '')
    if opposite(one) in results:
        ...
    else:
        f = False

if f:
    print("TRUE")
else:
    print("FALSE")
